ds,ds':fpf(Id; ltg.Type).
fpf-sub(Id; x.Type; id-deq; ds; ds')  subtype_rel(ma-state(ds'); ma-state(ds)) 

latex

Definitions	guard(T), fpf-sub(A; a.B(a); eq; f; g), id-deq, fpf(A; a.B(a)), ma-state(ds), P  Q, t  T, fpf-cap(f; eq; x; z), top, x. t(x), x:A. B(x), Id
Lemmas	subtype rel self, fpf-cap wf, top wf, subtype rel dep function, Id wf, fpf wf, id-deq wf, fpf-sub wf, subtype-fpf-cap